(set-logic HO_QF_UFLIA)
(set-info :status sat)
(declare-fun a () Int)
(declare-fun b (Int Int) Int)
(declare-fun c (Int Int) Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(assert (= d (b j d) a))
(assert (= e (c e i)))
(assert (= (b k f) a))
(assert (= d (+ g 4)))
(assert (= j (* g 5)))
(assert (= e (+ g 5)))
(assert (= k 0))
(check-sat)
